T, A:Type, l:IdLnk, ds:x:Id fp Type, P:(State(ds)AProp), f:(State(ds)AT).
Normal(A)
 Normal(T)
 Normal(ds)
 (s:State(ds). Dec(v:A. P(s,v)))
 at src(l):action a(m) precondition P sends [tg,f] on link l  Realizer 

latex

Definitions	Id, P  Q, at src(l):action $a(m) precondition P sends [$tg,f] on link l, Top, x:A. B(x), DeclaredType(ds;x), x:A. B(x), "$x", Prop, x. t(x), t  T, x(s), IdLnk
Lemmas	normal-ds wf, normal-type wf, decl-type wf, locl wf, decidable wf, IdLnk wf, fpf-single wf, Rlist wf, id-deq wf, Rpre wf, Knd wf, Rsframe wf, lsrc wf, fpf-cap-single1, Id wf, Rsends wf, decl-state wf, fpf wf, es realizer wf